#; ACL2 Version 2.5 -- A Computational Logic for Applicative Common Lisp
#; Copyright (C) 2000  University of Texas at Austin

#; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
#; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTES-2-0.

#; This program is free software; you can redistribute it and/or modify
#; it under the terms of the GNU General Public License as published by
#; the Free Software Foundation; either version 2 of the License, or
#; (at your option) any later version.

#; This program is distributed in the hope that it will be useful,
#; but WITHOUT ANY WARRANTY; without even the implied warranty of
#; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
#; GNU General Public License for more details.

#; You should have received a copy of the GNU General Public License
#; along with this program; if not, write to the Free Software
#; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

#; Written by:  Matt Kaufmann               and J Strother Moore
#; email:       Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu
#; Department of Computer Sciences
#; University of Texas at Austin
#; Austin, TX 78712-1188 U.S.A.

#; Adapted from makefiles for IHS and data-structures library, which were
#; created by Bishop Brock.

#; NOTE:  Target "all" causes a recursive invocation of make with ACL2 set to
#; its current value.  These recursive invocations of make thus have ACL2 set
#; on the command line, which overrides any values of ACL2 set in those files.
#; This should not cause any problems unless you try to do something fancy; see
#; the comment for example just above target .exercises.cert in
#; books/case-studies/ivy/ivy-v2/ivy-sources/Makefile from the ACL2
#; distribution.

#==============================================================================

BASE = /home/fmartin/Trabajo/investigacion/acl2

############################ Editable variables ###############################

# The ACL2 macro defines how to run ACL2.  The default command below prints
# runtime statistics for the certification, and runs it `nice' in an attempt to
# lessen interference with interactive jobs.  We normally inhibit most output
# during certification to speed up the proofs.  Edit as necessary.  The setting
# below reflects an assumption regarding where this makefile will be executed,
# namely, directly under books/.  This assumption can of course be overridden
# by specifying ACL2=acl2 (or change acl2 to your saved image) on the command
# line.

ACL2 = time nice acl2

# Fix problem with sh on some Linux systems:

ifeq ($(OSTYPE),linux)
	SHELL = bash
	ACL2 = acl2
endif
ifeq ($(OSTYPE),linux-gnu)
	SHELL = bash
	ACL2 = acl2
endif

# Inhibit all output.  Set this to "" if you do want the output.

#INHIBIT = (assign inhibit-output-lst \
#                  (list (quote prove) \
#                        (quote proof-tree) \
#                        (quote warning) \
#                        (quote observation)))

INHIBIT = ""

# Support for make dependencies:  should be a list of book names without
# the .lisp suffix.  Can be overridden on the command line or in a file
# that includes this file.

BOOKS = $(patsubst %.lisp, %, $(wildcard *.lisp))

DIRS = 

######################### END of editable variables ###########################

# We should really check that following is not empty.  It is the same as
# books, but with .cert suffixes.  This variable should not be overridden;
# it is computed as needed from BOOKS.

BOOKS_CERT = $(patsubst %, %.cert, $(BOOKS))

# This rule tells how to get <book>.cert from <book>.lisp, either by running
# Acl2 on the <book>.acl2 file (if it exists) or using the default command
# to certify at ground zero.

%.cert:
	echo "Making $(notdir $*).cert on `date`"
	date > $*.date
	echo '$(INHIBIT)' > $(dir $*)/workxxx
	sed --silent "/#|.*[cC]ert.*:/,/|#/ p" \
          $*.lisp | sed "/#|/ d" | sed "/|#/ d" >> $(dir $*)/workxxx
	(cd $(dir $*) ; \
	  $(ACL2) < workxxx > $(notdir $*).log)
	rm -f $(dir $*)/workxxx
	if \
	  [ -f $*.cert ] ; \
	then \
	  ls -al $*.cert ; \
	else \
	  echo 'The make for the book $(notdir $*).lisp seems to have failed.' ; \
	  rm $*.date ; \
	fi

# This rule certifies every book in BOOKS.  If the dependencies are set up
# correctly then the order of the books in BOOKS won't matter.

all:
	if \
	  [[ "$(BOOKS)" != "" ]] ; \
	then \
	  make -s -f Makefile $(BOOKS_CERT) INHIBIT='$(INHIBIT)' \
 	                       ACL2='$(ACL2)'; \
        fi
	@for dir in $(DIRS) ; \
	do \
	echo ; echo "Certifying the directory $$dir" ; \
	(cd $$dir ; \
	make ; \
	cd ..) ; \
	done

all-prove:
	@make -s -f Makefile $(BOOKS_CERT) INHIBIT='' ACL2='$(ACL2)'
	@for dir in $(DIRS) ; \
	do \
	echo ; echo "Certifying the directory $$dir" ; \
	(cd $$dir ; \
	make all-prove; \
	cd ..) ; \
	done

# This rule prints make dependency commands to the screen.  For best
# results run as `make -s dependencies'.

dependencies: 
	@for book in $(BOOKS) ; \
	do \
	(echo "" ;  echo "# - $$book" ; \
	egrep '^[^;]*(include-book|INCLUDE-BOOK)[ \t]*\".*\"' \
	`if [ -f $$book.acl2 ]; then echo "$$book.acl2"; fi` $$book.lisp) | \
	sed "s/[^\"]*\"/$$book.cert: DOLLAR(/" | \
        sed 's/DOLLAR(\([^\/]*\/\)*/$$(/' | sed 's/".*/)/' ;\
	done

# Clean:

# To clean the .date and .log files:

clean-log:
	@$(RM) $(RMFLAGS) $(BOOKS:=.log) $(BOOKS:=.date) *~

# To clean the .cert, .o, .date, files:

clean:
	@make clean-log
	@$(RM) $(RMFLAGS) $(BOOKS:=.cert) $(BOOKS:=.o) $(BOOKS:=.h) \
               $(BOOKS:=.c) $(BOOKS:=.data) $(BOOKS:=.x86f) \
               $(BOOKS:=.fas) $(BOOKS:=.lib) $(BOOKS:=.out)
	@for dir in $(DIRS) ; \
	do \
	echo ; echo "Cleaning the directory $$dir" ; \
	(cd $$dir ; \
	make clean; \
	cd ..) ; \
	done

#==============================================================================
